\begin{tabbing}
$\forall$${\it es}$:event\_system\{i:l\}, $T$:Type, $c$:$T$, $i$,$x$:Id.
\\[0ex]init{-}p(${\it es}$; $i$; $T$; $x$; $c$)
\\[0ex]$\Rightarrow$ guard(\=(es{-}dtype(${\it es}$; $i$; $x$; $T$)\+
\\[0ex]c$\wedge$ alle{-}at(${\it es}$; $i$; $e$.(($\uparrow$es{-}first(${\it es}$; $e$)) $\Rightarrow$ (es{-}when(${\it es}$; $x$; $e$) = $c$ $\in$ $T$)))))
\-
\end{tabbing}